$\forall$$p$,$q$:($n$:$\mathbb{Z}$ $\times$ base{-}domain{-}type($n$)). ($\uparrow$eq\_bd($p$; $q$)) $\Leftarrow\!\Rightarrow$ ($p$ = $q$)